COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Title: Basic Research in Artificial Intelligence
C00007 00003	Notes for NSF proposal
C00008 ENDMK
C⊗;
Title: Basic Research in Artificial Intelligence

	This is a request for a continuing grant of xxx per year
in support of basic research in artificial intelligence
with emphasis on the structure of formal reasoning and
computer proof checking.  The computer proof checking supports the
basic research in AI, but also has applications to verifying
computer programs and is independently valuable.


Introduction

	Artificial intelligence has proved to be a difficult branch
of science.  Some people thought that human level intelligence
could be achieved in ten or twenty years, but this was based on
the difficulties they could see when they made the optimistic
predictions.  Our own opinion is that major scientific discoveries
remain to be made.
Moreover, many of these discoveries require theoretical advances and
not merely the extension of current ideas for producing "expert programs"
to new domains.
The increasing emphasis by ARPA and other agencies sponsoring AI
research on immediate applications has resulted in a serious
imbalance.  Deciding what the basic issues are is difficult
enough without having formulate everything in terms of demonstration
programs to be available in two years.

	Our research is based on the idea that for many purposes,
the problems of artificial intelligence can be separated into two
parts - an epistemological part and a heuristic part.
The %2epistemological%1 part concerns what facts and inference
rules are available for solving a problem and how they can be
represented in the memory of a computer, and the heuristic part
concerns procedures for deciding what to do on the basis of the
necessary facts.  Most work in AI has concerned the %2heuristics%1,
and computer representations of information have been chosen that
are capable of representing only a part of the information that
would be available to a human.  The modes of reasoning used by
present programs are often even weaker than the representations
themselves.

xxxx

PROOF CHECKING BY COMPUTER

	We must distinguish theorem proving by computer from proof-checking
by computer.

	It is an essential part of the notion of proof in a formal
system that a candidate proof can be checked by a mechanical process.
It is a consequence of the work of Goedel, Church and Turing that
no mechanical process can always determine whether a proof of a
given sentence exists in a formal system.
In principle, therefore, proof-checking should be easy, while all
the difficulties of understanding the creative processes of a
mathematician are involved in making a high powered theorem prover.

Notes for NSF proposal

What: Proof checking, epistemology, general basic research.

What has been done: LCF, FOL, McCs epistemology and MTC.

Who: Weyhrauch, JMC part time, research fellow as visitor, 4 graduate
students, disk file, terminals.

Publications: